경량 형식적 방법론
- 2025-07-12
대니얼 잭슨이 1996년에 고안한 용어.1 Alloy 등을 활용하여 빠르게 피드백을 받아가며 점진적으로 모델을 다듬어가는 방식.
Models are developed incrementally, driven by the modeler’s perception of which aspects of the software matter most, and of where the greatest risks lie, and automated tools are exploited to find flaws as early as possible. —Software Abstractions: Logic, Language, and Analysis
Elements
경량 형식적 방법론을 “경량”이게 하는 요소들:
- Paritiality in language: 표현력을 높이기 위해 언어를 복잡하게 만드는 대신 표현력을 제한하고 언어를 단순화하기
- Partiality in modeling: 전체 시스템 중에서 필요한 부분만 형식화하기
- Partiaility in analysis: 분석의 범위를 제한하되 해당 범위 안에서는 모든 케이스를 검사하기 (참고: Small scope hypothesis)
- Partiaility in composition: 부분적인 명세를 조합하기